Termination proof of /tmp/tmpNV7LIz/OvConsOS

Termination of the following Term Rewriting System could not be shown:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U12: {1}
s: {1}
length: {1}
U21: {1}
U22: {1}
U23: {1}
take: {1, 2}
nil: empty set

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U12: {1}
s: {1}
length: {1}
U21: {1}
U22: {1}
U23: {1}
take: {1, 2}
nil: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The replacement map contains the following entries:

zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
U12: {1}
s: {1}
length: {1}
U21: {1}
U22: {1}
U23: {1}
take: {1, 2}
nil: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, take, LENGTH, TAKE} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U23, U12¹, U11¹, U22¹, U21¹, U23¹} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

U11¹(tt, L) → U12¹(tt, L)
U12¹(tt, L) → LENGTH(L)
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
LENGTH(cons(N, L)) → U11¹(tt, L)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)

The collapsing dependency pairs are DP_c:

U12¹(tt, L) → L
U23¹(tt, IL, M, N) → N

The hidden terms of R are:

zeros
take(M, IL)

Every hiding context is built from:

take on positions {1, 2}

Hence, the new unhiding pairs DP_u are :

U12¹(tt, L) → U(L)
U23¹(tt, IL, M, N) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(zeros) → ZEROS
U(take(M, IL)) → TAKE(M, IL)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(nil)
length(cons(x0, x1))
take(0, x0)
take(s(x0), cons(x1, x2))

The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 2 less nodes.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, take, TAKE} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U23, U23¹, U22¹, U21¹} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → U(N)
U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(nil)
length(cons(x0, x1))
take(0, x0)
take(s(x0), cons(x1, x2))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(take(x_0, x_1)) → U(x_0)
U(take(x_0, x_1)) → U(x_1)
U(take(M, IL)) → TAKE(M, IL)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)

The remaining pairs can at least be oriented weakly.

U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → U(N)
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)

Used ordering: Combined order from the following AFS and order.
U23¹(x1, x2, x3, x4) = x4
U22¹(x1, x2, x3, x4) = x4
U(x1) = x1
TAKE(x1, x2) = x2
U21¹(x1, x2, x3, x4) = x4

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ QCSDependencyGraphProof

              ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, take} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U23, U23¹, U22¹, U21¹} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → U(N)
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(nil)
length(cons(x0, x1))
take(0, x0)
take(s(x0), cons(x1, x2))

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ ConvertedToQDPProblemProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {s, length, take, LENGTH} are replacing on all positions.
For all symbols f in {cons, U11, U12, U21, U22, U23, U12¹, U11¹} we have µ(f) = {1}.

The TRS P consists of the following rules:

U12¹(tt, L) → LENGTH(L)
LENGTH(cons(N, L)) → U11¹(tt, L)
U11¹(tt, L) → U12¹(tt, L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(nil)
length(cons(x0, x1))
take(0, x0)
take(s(x0), cons(x1, x2))

Converted QDP Problem, but could not keep Q or minimality.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ ConvertedToQDPProblemProof

                  ↳ QDP

                    ↳ NonTerminationProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(tt, L)
U11¹(tt, L) → U12¹(tt, L)
U12¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(tt, L)
U11¹(tt, L) → U12¹(tt, L)
U12¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

s = U11¹(tt, zeros) evaluates to t =U11¹(tt, zeros)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [ ]

Rewriting sequence

U11¹(tt, zeros) → U11¹(tt, cons(0, zeros))
with rule zeros → cons(0, zeros) at position [1] and matcher [ ]

U11¹(tt, cons(0, zeros)) → U12¹(tt, cons(0, zeros))
with rule U11¹(tt, L') → U12¹(tt, L') at position [] and matcher [L' / cons(0, zeros)]

U12¹(tt, cons(0, zeros)) → LENGTH(cons(0, zeros))
with rule U12¹(tt, L') → LENGTH(L') at position [] and matcher [L' / cons(0, zeros)]

LENGTH(cons(0, zeros)) → U11¹(tt, zeros)
with rule LENGTH(cons(N, L)) → U11¹(tt, L)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(0, IL) → nil
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(nil) → 0
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(0, IL) → nil
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

lengthActive(nil) → 0

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U12(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U12Active(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(U21(x₁, x₂, x₃, x₄)) = 2·x₁ + x₂ + x₃ + 2·x₄
POL(U21Active(x₁, x₂, x₃, x₄)) = 2·x₁ + x₂ + x₃ + 2·x₄
POL(U22(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + 2·x₄
POL(U22Active(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + 2·x₄
POL(U23(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + 2·x₄
POL(U23Active(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + 2·x₄
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(length(x₁)) = 1 + 2·x₁
POL(lengthActive(x₁)) = 1 + 2·x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = x₁ + x₂
POL(takeActive(x₁, x₂)) = x₁ + x₂
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(0, IL) → nil
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(0, IL) → nil
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

takeActive(0, IL) → nil

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + 2·x₂
POL(U11Active(x₁, x₂)) = x₁ + 2·x₂
POL(U12(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U12Active(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U21(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + x₂ + 2·x₃ + x₄
POL(U21Active(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + x₂ + 2·x₃ + x₄
POL(U22(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + x₄
POL(U22Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + x₄
POL(U23(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + x₄
POL(U23Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + x₄
POL(cons(x₁, x₂)) = x₁ + x₂
POL(length(x₁)) = 2·x₁
POL(lengthActive(x₁)) = 2·x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(U22(x1, x2, x3, x4)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(take(x1, x2)) → MARK(x2)
MARK(U11(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
TAKEACTIVE(s(M), cons(N, IL)) → U21ACTIVE(tt, IL, M, N)
U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(zeros) → ZEROSACTIVE
MARK(length(x1)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
U12ACTIVE(tt, L) → MARK(L)
MARK(U23(x1, x2, x3, x4)) → MARK(x1)
MARK(U22(x1, x2, x3, x4)) → U22ACTIVE(mark(x1), x2, x3, x4)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U23ACTIVE(tt, IL, M, N) → MARK(N)
MARK(U12(x1, x2)) → U12ACTIVE(mark(x1), x2)
MARK(U21(x1, x2, x3, x4)) → U21ACTIVE(mark(x1), x2, x3, x4)
MARK(U12(x1, x2)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
U21ACTIVE(tt, IL, M, N) → U22ACTIVE(tt, IL, M, N)
MARK(U23(x1, x2, x3, x4)) → U23ACTIVE(mark(x1), x2, x3, x4)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1, x2, x3, x4)) → MARK(x1)
U22ACTIVE(tt, IL, M, N) → U23ACTIVE(tt, IL, M, N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(U22(x1, x2, x3, x4)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(take(x1, x2)) → MARK(x2)
MARK(U11(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
TAKEACTIVE(s(M), cons(N, IL)) → U21ACTIVE(tt, IL, M, N)
U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
MARK(zeros) → ZEROSACTIVE
MARK(length(x1)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
U12ACTIVE(tt, L) → MARK(L)
MARK(U23(x1, x2, x3, x4)) → MARK(x1)
MARK(U22(x1, x2, x3, x4)) → U22ACTIVE(mark(x1), x2, x3, x4)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U23ACTIVE(tt, IL, M, N) → MARK(N)
MARK(U12(x1, x2)) → U12ACTIVE(mark(x1), x2)
MARK(U21(x1, x2, x3, x4)) → U21ACTIVE(mark(x1), x2, x3, x4)
MARK(U12(x1, x2)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
U21ACTIVE(tt, IL, M, N) → U22ACTIVE(tt, IL, M, N)
MARK(U23(x1, x2, x3, x4)) → U23ACTIVE(mark(x1), x2, x3, x4)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1, x2, x3, x4)) → MARK(x1)
U22ACTIVE(tt, IL, M, N) → U23ACTIVE(tt, IL, M, N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(U22(x1, x2, x3, x4)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(take(x1, x2)) → MARK(x2)
MARK(U11(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
TAKEACTIVE(s(M), cons(N, IL)) → U21ACTIVE(tt, IL, M, N)
MARK(length(x1)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
U12ACTIVE(tt, L) → MARK(L)
MARK(U23(x1, x2, x3, x4)) → MARK(x1)
MARK(U22(x1, x2, x3, x4)) → U22ACTIVE(mark(x1), x2, x3, x4)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U23ACTIVE(tt, IL, M, N) → MARK(N)
MARK(U12(x1, x2)) → U12ACTIVE(mark(x1), x2)
MARK(U21(x1, x2, x3, x4)) → U21ACTIVE(mark(x1), x2, x3, x4)
MARK(U12(x1, x2)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
U21ACTIVE(tt, IL, M, N) → U22ACTIVE(tt, IL, M, N)
MARK(U23(x1, x2, x3, x4)) → U23ACTIVE(mark(x1), x2, x3, x4)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1, x2, x3, x4)) → MARK(x1)
U22ACTIVE(tt, IL, M, N) → U23ACTIVE(tt, IL, M, N)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(U22(x1, x2, x3, x4)) → MARK(x1)
MARK(length(x1)) → LENGTHACTIVE(mark(x1))
MARK(take(x1, x2)) → MARK(x2)
MARK(U11(x1, x2)) → MARK(x1)
MARK(length(x1)) → MARK(x1)
MARK(take(x1, x2)) → MARK(x1)
MARK(U23(x1, x2, x3, x4)) → MARK(x1)
MARK(U22(x1, x2, x3, x4)) → U22ACTIVE(mark(x1), x2, x3, x4)
MARK(U12(x1, x2)) → U12ACTIVE(mark(x1), x2)
MARK(U21(x1, x2, x3, x4)) → U21ACTIVE(mark(x1), x2, x3, x4)
MARK(U12(x1, x2)) → MARK(x1)
MARK(U11(x1, x2)) → U11ACTIVE(mark(x1), x2)
MARK(U23(x1, x2, x3, x4)) → U23ACTIVE(mark(x1), x2, x3, x4)
MARK(take(x1, x2)) → TAKEACTIVE(mark(x1), mark(x2))
MARK(U21(x1, x2, x3, x4)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L))
TAKEACTIVE(s(M), cons(N, IL)) → U21ACTIVE(tt, IL, M, N)
U12ACTIVE(tt, L) → MARK(L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U23ACTIVE(tt, IL, M, N) → MARK(N)
U21ACTIVE(tt, IL, M, N) → U22ACTIVE(tt, IL, M, N)
U22ACTIVE(tt, IL, M, N) → U23ACTIVE(tt, IL, M, N)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(TAKEACTIVE(x₁, x₂)) = x₂
POL(U11(x₁, x₂)) = 1 + x₁ + x₂
POL(U11ACTIVE(x₁, x₂)) = x₂
POL(U11Active(x₁, x₂)) = 1 + x₁ + x₂
POL(U12(x₁, x₂)) = 1 + x₁ + x₂
POL(U12ACTIVE(x₁, x₂)) = x₂
POL(U12Active(x₁, x₂)) = 1 + x₁ + x₂
POL(U21(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(U21ACTIVE(x₁, x₂, x₃, x₄)) = x₂ + x₄
POL(U21Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(U22(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(U22ACTIVE(x₁, x₂, x₃, x₄)) = x₄
POL(U22Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(U23(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(U23ACTIVE(x₁, x₂, x₃, x₄)) = x₄
POL(U23Active(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + x₃ + x₄
POL(cons(x₁, x₂)) = x₁ + x₂
POL(length(x₁)) = 1 + x₁
POL(lengthActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(takeActive(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

U12Active(x1, x2) → U12(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
zerosActive → zeros
mark(zeros) → zerosActive
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(s(x1)) → MARK(x1)
U22ACTIVE(tt, IL, M, N) → U23ACTIVE(tt, IL, M, N)
U21ACTIVE(tt, IL, M, N) → U22ACTIVE(tt, IL, M, N)
MARK(cons(x1, x2)) → MARK(x1)
U12ACTIVE(tt, L) → MARK(L)
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U23ACTIVE(tt, IL, M, N) → MARK(N)
TAKEACTIVE(s(M), cons(N, IL)) → U21ACTIVE(tt, IL, M, N)
U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 5 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ UsableRulesProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                              ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(s(x1)) → MARK(x1)
MARK(cons(x1, x2)) → MARK(x1)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MARK(s(x1)) → MARK(x1)
The graph contains the following edges 1 > 1
MARK(cons(x1, x2)) → MARK(x1)
The graph contains the following edges 1 > 1

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U12ACTIVE(tt, L) → LENGTHACTIVE(mark(L)) at position [0] we obtained the following new rules:

U12ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U12ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, 0) → LENGTHACTIVE(0)
U12ACTIVE(tt, U12(x0, x1)) → LENGTHACTIVE(U12Active(mark(x0), x1))
U12ACTIVE(tt, s(x0)) → LENGTHACTIVE(s(mark(x0)))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U12ACTIVE(tt, nil) → LENGTHACTIVE(nil)
U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, tt) → LENGTHACTIVE(tt)
U12ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U12ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U12ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, 0) → LENGTHACTIVE(0)
U12ACTIVE(tt, U12(x0, x1)) → LENGTHACTIVE(U12Active(mark(x0), x1))
U12ACTIVE(tt, s(x0)) → LENGTHACTIVE(s(mark(x0)))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U12ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)
U12ACTIVE(tt, nil) → LENGTHACTIVE(nil)
U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, tt) → LENGTHACTIVE(tt)
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U12ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U12(x0, x1)) → LENGTHACTIVE(U12Active(mark(x0), x1))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule U12ACTIVE(tt, zeros) → LENGTHACTIVE(zerosActive) at position [0] we obtained the following new rules:

U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(zeros)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U12ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U12ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U12(x0, x1)) → LENGTHACTIVE(U12Active(mark(x0), x1))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U12ACTIVE(tt, zeros) → LENGTHACTIVE(zeros)
U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U12ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U12ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U12(x0, x1)) → LENGTHACTIVE(U12Active(mark(x0), x1))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U12ACTIVE(tt, cons(x0, x1)) → LENGTHACTIVE(cons(mark(x0), x1))
U12ACTIVE(tt, U11(x0, x1)) → LENGTHACTIVE(U11Active(mark(x0), x1))
U12ACTIVE(tt, length(x0)) → LENGTHACTIVE(lengthActive(mark(x0)))
U12ACTIVE(tt, U12(x0, x1)) → LENGTHACTIVE(U12Active(mark(x0), x1))

The remaining pairs can at least be oriented weakly.

U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11ACTIVE(x₁, x₂)) = 1 + x₂
POL(U11Active(x₁, x₂)) = 0
POL(U12(x₁, x₂)) = 0
POL(U12ACTIVE(x₁, x₂)) = 1 + x₂
POL(U12Active(x₁, x₂)) = 0
POL(U21(x₁, x₂, x₃, x₄)) = 0
POL(U21Active(x₁, x₂, x₃, x₄)) = 1
POL(U22(x₁, x₂, x₃, x₄)) = 0
POL(U22Active(x₁, x₂, x₃, x₄)) = 1
POL(U23(x₁, x₂, x₃, x₄)) = 0
POL(U23Active(x₁, x₂, x₃, x₄)) = 1
POL(cons(x₁, x₂)) = 1 + x₂
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1 + x₁
POL(nil) = 0
POL(s(x₁)) = 0
POL(take(x₁, x₂)) = 0
POL(takeActive(x₁, x₂)) = 1
POL(tt) = 0
POL(zeros) = 1
POL(zerosActive) = 0

The following usable rules [17] were oriented:

U12Active(x1, x2) → U12(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
mark(s(x1)) → s(mark(x1))
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U12ACTIVE(tt, U22(x0, x1, x2, x3)) → LENGTHACTIVE(U22Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U21(x0, x1, x2, x3)) → LENGTHACTIVE(U21Active(mark(x0), x1, x2, x3))
U12ACTIVE(tt, U23(x0, x1, x2, x3)) → LENGTHACTIVE(U23Active(mark(x0), x1, x2, x3))

The remaining pairs can at least be oriented weakly.

U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)

Used ordering: Polynomial interpretation [25]:

POL(0) = 0
POL(LENGTHACTIVE(x₁)) = x₁
POL(U11(x₁, x₂)) = 0
POL(U11ACTIVE(x₁, x₂)) = 1 + x₂
POL(U11Active(x₁, x₂)) = 0
POL(U12(x₁, x₂)) = 0
POL(U12ACTIVE(x₁, x₂)) = 1 + x₂
POL(U12Active(x₁, x₂)) = 0
POL(U21(x₁, x₂, x₃, x₄)) = 1
POL(U21Active(x₁, x₂, x₃, x₄)) = 1
POL(U22(x₁, x₂, x₃, x₄)) = 1
POL(U22Active(x₁, x₂, x₃, x₄)) = 1
POL(U23(x₁, x₂, x₃, x₄)) = 1
POL(U23Active(x₁, x₂, x₃, x₄)) = 1
POL(cons(x₁, x₂)) = 1 + x₂
POL(length(x₁)) = 0
POL(lengthActive(x₁)) = 0
POL(mark(x₁)) = 1 + x₁
POL(nil) = 0
POL(s(x₁)) = 0
POL(take(x₁, x₂)) = 0
POL(takeActive(x₁, x₂)) = 1
POL(tt) = 0
POL(zeros) = 0
POL(zerosActive) = 0

The following usable rules [17] were oriented:

U12Active(x1, x2) → U12(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
lengthActive(x1) → length(x1)
mark(length(x1)) → lengthActive(mark(x1))
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
mark(s(x1)) → s(mark(x1))
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ DependencyGraphProof

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ DependencyGraphProof

                                              ↳ QDP

                                                ↳ QDPOrderProof

                                                  ↳ QDP

                                                    ↳ QDPOrderProof

                                                      ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

U12ACTIVE(tt, take(x0, x1)) → LENGTHACTIVE(takeActive(mark(x0), mark(x1)))
U12ACTIVE(tt, zeros) → LENGTHACTIVE(cons(0, zeros))
LENGTHACTIVE(cons(N, L)) → U11ACTIVE(tt, L)
U11ACTIVE(tt, L) → U12ACTIVE(tt, L)

The TRS R consists of the following rules:

mark(zeros) → zerosActive
zerosActive → zeros
mark(U11(x1, x2)) → U11Active(mark(x1), x2)
U11Active(x1, x2) → U11(x1, x2)
mark(U12(x1, x2)) → U12Active(mark(x1), x2)
U12Active(x1, x2) → U12(x1, x2)
mark(U21(x1, x2, x3, x4)) → U21Active(mark(x1), x2, x3, x4)
U21Active(x1, x2, x3, x4) → U21(x1, x2, x3, x4)
mark(U22(x1, x2, x3, x4)) → U22Active(mark(x1), x2, x3, x4)
U22Active(x1, x2, x3, x4) → U22(x1, x2, x3, x4)
mark(U23(x1, x2, x3, x4)) → U23Active(mark(x1), x2, x3, x4)
U23Active(x1, x2, x3, x4) → U23(x1, x2, x3, x4)
mark(length(x1)) → lengthActive(mark(x1))
lengthActive(x1) → length(x1)
mark(take(x1, x2)) → takeActive(mark(x1), mark(x2))
takeActive(x1, x2) → take(x1, x2)
mark(cons(x1, x2)) → cons(mark(x1), x2)
mark(0) → 0
mark(tt) → tt
mark(s(x1)) → s(mark(x1))
mark(nil) → nil
zerosActive → cons(0, zeros)
U11Active(tt, L) → U12Active(tt, L)
U12Active(tt, L) → s(lengthActive(mark(L)))
U21Active(tt, IL, M, N) → U22Active(tt, IL, M, N)
U22Active(tt, IL, M, N) → U23Active(tt, IL, M, N)
U23Active(tt, IL, M, N) → cons(mark(N), take(M, IL))
lengthActive(cons(N, L)) → U11Active(tt, L)
takeActive(s(M), cons(N, IL)) → U21Active(tt, IL, M, N)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Trivial transformation to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(nil) → 0
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

length(nil) → 0

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = 2·x₁ + x₂
POL(U12(x₁, x₂)) = x₁ + x₂
POL(U21(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + x₂ + 2·x₃ + 2·x₄
POL(U22(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + 2·x₄
POL(U23(x₁, x₂, x₃, x₄)) = 1 + x₁ + x₂ + 2·x₃ + 2·x₄
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(length(x₁)) = x₁
POL(nil) = 1
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(0, IL) → nil
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

take(0, IL) → nil

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(U11(x₁, x₂)) = x₁ + x₂
POL(U12(x₁, x₂)) = 2·x₁ + x₂
POL(U21(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + x₂ + x₃ + 2·x₄
POL(U22(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + x₂ + x₃ + 2·x₄
POL(U23(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + x₂ + x₃ + 2·x₄
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(length(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(take(x₁, x₂)) = 1 + x₁ + x₂
POL(tt) = 0
POL(zeros) = 0

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → TAKE(M, IL)
LENGTH(cons(N, L)) → U11¹(tt, L)
U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)
U12¹(tt, L) → LENGTH(L)
U11¹(tt, L) → U12¹(tt, L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → TAKE(M, IL)
LENGTH(cons(N, L)) → U11¹(tt, L)
U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)
U12¹(tt, L) → LENGTH(L)
U11¹(tt, L) → U12¹(tt, L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                            ↳ UsableRulesProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → TAKE(M, IL)
U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → TAKE(M, IL)
U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)

R is empty.
The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
U23¹(tt, IL, M, N) → TAKE(M, IL)
U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)

From the DPs we obtained the following set of size-change graphs:

U22¹(tt, IL, M, N) → U23¹(tt, IL, M, N)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
TAKE(s(M), cons(N, IL)) → U21¹(tt, IL, M, N)
The graph contains the following edges 2 > 2, 1 > 3, 2 > 4
U23¹(tt, IL, M, N) → TAKE(M, IL)
The graph contains the following edges 3 >= 1, 2 >= 2
U21¹(tt, IL, M, N) → U22¹(tt, IL, M, N)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(tt, L)
U11¹(tt, L) → U12¹(tt, L)
U12¹(tt, L) → LENGTH(L)

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(tt, L)
U11¹(tt, L) → U12¹(tt, L)
U12¹(tt, L) → LENGTH(L)

R is empty.
The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(tt, L)
U12¹(tt, L) → LENGTH(L)
U11¹(tt, L) → U12¹(tt, L)

From the DPs we obtained the following set of size-change graphs:

U11¹(tt, L) → U12¹(tt, L)
The graph contains the following edges 1 >= 1, 2 >= 2
U12¹(tt, L) → LENGTH(L)
The graph contains the following edges 2 >= 1
LENGTH(cons(N, L)) → U11¹(tt, L)
The graph contains the following edges 1 > 2

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

The TRS R consists of the following rules:

zeros → cons(0, zeros)
U11(tt, L) → U12(tt, L)
U12(tt, L) → s(length(L))
U21(tt, IL, M, N) → U22(tt, IL, M, N)
U22(tt, IL, M, N) → U23(tt, IL, M, N)
U23(tt, IL, M, N) → cons(N, take(M, IL))
length(cons(N, L)) → U11(tt, L)
take(s(M), cons(N, IL)) → U21(tt, IL, M, N)

The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

R is empty.
The set Q consists of the following terms:

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

zeros
U11(tt, x0)
U12(tt, x0)
U21(tt, x0, x1, x2)
U22(tt, x0, x1, x2)
U23(tt, x0, x1, x2)
length(cons(x0, x1))
take(s(x0), cons(x1, x2))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ Overlay + Local Confluence

                ↳ QTRS

                  ↳ DependencyPairsProof

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ZEROS → ZEROS

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.